fixed bug

src/cfg.ml

@@ -225,7 +225,7 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
       cfgBlock blk (Some s) next (Some s) nodeList rlabels
       (* Since all loops have terminating condition true, we don't put
          any direct successor to stmt following the loop *)
-  | Asm _ -> addOptionSucc next (* the extra edges are added inside goblint's cfg *)
+  | Asm (_, _, _, _, _, labels, _) -> addOptionSucc next (* the extra edges are added inside goblint's cfg *)
 
 (*------------------------------------------------------------*)
 

src/check.ml

@@ -809,7 +809,17 @@ and checkStmt (s: stmt) =
             cases;
 
       | Instr il -> List.iter checkInstr il
-      | Asm _ -> ()  (* Not yet implemented *)
+      | Asm (_, _, _, _, _, labels, l) ->
+        currentLoc := l;
+        List.iter (fun dest ->
+          List.iter (fun label ->
+            let name = match label with
+              | Label (name, _, true) -> name
+              | _ -> failwith "unreachable"
+            in
+            gotoTargets := (name, !dest) :: !gotoTargets
+          ) !dest.labels;
+        ) labels;
       )
     () (* argument of withContext *)
 

src/cil.ml

@@ -6550,7 +6550,11 @@ and succpred_stmt s fallthrough rlabels =
                 | hd :: tl -> link s hd ;
                     succpred_block b fallthrough rlabels
                 end
-  | Asm _ -> trylink s fallthrough
+  | Asm (_, _, _, _, _, labels, _) -> 
+      List.iter (fun label ->
+        link s !label
+      ) labels;
+      trylink s fallthrough
 
 
 let caseRangeFold (l: label list) =

src/rmUnused.ml

@@ -642,7 +642,14 @@ class markUsedLabels (labelMap: (string, unit) H.t) = object
         (* Mark it as used *)
         H.replace labelMap ln ();
         DoChildren
-
+    | Asm (_, _, _, _, _, labels, _) ->
+        List.iter (fun dest ->
+          let (ln, _, _), _ = labelsToKeep !dest.labels in
+          if ln = "" then
+            E.s (E.bug "rmUnused: destination of statement does not have labels");
+          H.replace labelMap ln ();
+        ) labels;
+        DoChildren
     | _ -> DoChildren
 
   method! vexpr e = match e with

test/small1/asm_goto3.c

@@ -1,6 +1,6 @@
 #include "testharness.h"
 
-void code() {
+int main(void) {
 start:
   asm goto ("nop" : : : : start, exit);
 exit: