went through everything

Author: Simon Tietz

src/cdomain/value/cdomains/valueDomain.ml

@@ -725,7 +725,7 @@ struct
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
     |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
-    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *)
+    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 

src/common/framework/edge.ml

@@ -23,7 +23,8 @@ type t =
   (** The true-branch or false-branch of a conditional exp *)
   | ASM of string list * asm_out * asm_in * bool
   (** Inline assembly statements, and the annotations for output and input
-    * variables. The last field is a flag that indicates if this is a duplicated edge. *)
+    * variables. The last field is a flag that indicates if this is an edge that
+    * was inserted because of asm goto labels. *)
   | VDecl of CilType.Varinfo.t
   (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
     * local variables or only when it is not possible to pull the declaration up, is

src/config/options.schema.json

@@ -19,7 +19,7 @@
     },
     "asm_is_nop": {
       "title": "asm_is_nop",
-      "description": "treat asm statements as nop",
+      "description": "Treat assembly statements as NOOP",
       "type": "boolean",
       "default": true
     },

src/framework/constraints.ml

@@ -775,14 +775,14 @@ struct
 
   let tf var getl sidel getg sideg prev_node edge d =
     begin match edge with
-      | Assign (lv,rv) -> tf_assign var edge prev_node lv rv
-      | VDecl (v)      -> tf_vdecl var edge prev_node v
-      | Proc (r,f,ars) -> tf_proc var edge prev_node r f ars
-      | Entry f        -> tf_entry var edge prev_node f
-      | Ret (r,fd)     -> tf_ret var edge prev_node r fd
-      | Test (p,b)     -> tf_test var edge prev_node p b
-      | ASM (_, _, _,_)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
-      | Skip           -> tf_skip var edge prev_node
+      | Assign (lv,rv)  -> tf_assign var edge prev_node lv rv
+      | VDecl (v)       -> tf_vdecl var edge prev_node v
+      | Proc (r,f,ars)  -> tf_proc var edge prev_node r f ars
+      | Entry f         -> tf_entry var edge prev_node f
+      | Ret (r,fd)      -> tf_ret var edge prev_node r fd
+      | Test (p,b)      -> tf_test var edge prev_node p b
+      | ASM (_, _, _,_) -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
+      | Skip            -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
   type Goblint_backtrace.mark += TfLocation of location

src/maingoblint.ml

@@ -573,7 +573,7 @@ let do_analyze change_info merged_AST =
         (* Cilfacade.current_file := ast'; *)
     in
 
-    Timing.wrap "analysis" (control_analyze merged_AST) funs 
+    Timing.wrap "analysis" (control_analyze merged_AST) funs
   )
 
 let do_html_output () =