@@ -1735,21 +1735,16 @@ struct
17351735      match  Addr. to_mval x with 
17361736      |  Some  x  -> update_one_addr x store
17371737      |  None  -> store
1738-     in  try 
1739-       (*  We start from the current state and an empty list of global deltas,
1740-        * and we assign to all the the different possible places: *)  
1741-       let  nst =  AD. fold update_one lval st in 
1742-       (*  if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) 
1743-       (*  If the address was definite, then we just return it. If the address
1744-        * was ambiguous, we have to join it with the initial state. *)  
1745-       let  nst =  if  AD. cardinal lval >  1  then  D. join st nst else  nst in 
1746-       (*  if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) 
1747-       nst
1748-     with 
1749-     (*  If any of the addresses are unknown, we ignore it!?! *) 
1750-     |  SetDomain. Unsupported  x  ->
1751-       (*  if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'" x; *) 
1752-       M. info ~category: Unsound  " Assignment to unknown address, assuming no write happened." 
1738+     in  
1739+     (*  We start from the current state and an empty list of global deltas,
1740+       * and we assign to all the the different possible places: *)  
1741+     let  nst =  AD. fold update_one lval st in 
1742+     (*  if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) 
1743+     (*  If the address was definite, then we just return it. If the address
1744+       * was ambiguous, we have to join it with the initial state. *)  
1745+     let  nst =  if  AD. cardinal lval >  1  then  D. join st nst else  nst in 
1746+     (*  if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) 
1747+     nst
17531748
17541749  let  set_many  ~ctx   (st : store ) lval_value_list : store  = 
17551750    (*  Maybe this can be done with a simple fold *) 
0 commit comments