Merge pull request #51 from goblint/loc-end

Add end locations to statements

Author: sim642

CHANGES

@@ -1,3 +1,9 @@
+## Unreleased
+* Add ends to locations, allowing for ranges.
+* Add additional expression locations to statements, etc.
+
+## Older versions
+
 18 November 2021: goblint-cil-1.8.2
 
     * Add columns to locations.

src/cfg.ml

@@ -84,10 +84,10 @@ class caseLabeledStmtFinder slr = object(self)
         then begin
             slr := s :: (!slr);
             match s.skind with
-            | Switch(_,_,_,_) -> SkipChildren
+            | Switch(_,_,_,_,_) -> SkipChildren
             | _ -> DoChildren
         end else match s.skind with
-        | Switch(_,_,_,_) -> SkipChildren
+        | Switch(_,_,_,_,_) -> SkipChildren
         | _ -> DoChildren
 end
 
@@ -180,10 +180,10 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
     | hd::_ -> addSucc hd
   in
   let instrFallsThrough (i : instr) : bool = match i with
-      Call (_, Lval (Var vf, NoOffset), _, _) ->
+      Call (_, Lval (Var vf, NoOffset), _, _, _) ->
         (* See if this has the noreturn attribute *)
         not (hasAttribute "noreturn" vf.vattr)
-    | Call (_, f, _, _) ->
+    | Call (_, f, _, _, _) ->
         not (hasAttribute "noreturn" (typeAttrs (typeOf f)))
     | _ -> true
   in
@@ -198,7 +198,7 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
   | ComputedGoto (e,_) -> List.iter addSucc rlabels
   | Break _ -> addOptionSucc break
   | Continue _ -> addOptionSucc cont
-  | If (_, blk1, blk2, _) ->
+  | If (_, blk1, blk2, _, _) ->
       (* The succs of If is [true branch;false branch] *)
       addBlockSucc blk2 next;
       addBlockSucc blk1 next;
@@ -207,7 +207,7 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
   | Block b ->
       addBlockSucc b next;
       cfgBlock b next break cont nodeList rlabels
-  | Switch(_,blk,l,_) ->
+  | Switch(_,blk,l,_,_) ->
       let bl = findCaseLabeledStmts blk in
       List.iter addSucc (List.rev bl(*l*)); (* Add successors in order *)
       (* sfg: if there's no default, need to connect s->next *)
@@ -219,8 +219,8 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
       then
         addOptionSucc next;
       cfgBlock blk next next cont nodeList rlabels
-  | Loop(blk, loc, s1, s2) ->
-      s.skind <- Loop(blk, loc, (Some s), next);
+  | Loop(blk, loc, eloc, s1, s2) ->
+      s.skind <- Loop(blk, loc, eloc, (Some s), next);
       addBlockSucc blk (Some s);
       cfgBlock blk (Some s) next (Some s) nodeList rlabels
       (* Since all loops have terminating condition true, we don't put
@@ -246,9 +246,9 @@ and fasStmt (todo) (s : stmt) =
     ignore(todo s);
     match s.skind with
       | Block b -> fasBlock todo b
-      | If (_, tb, fb, _) -> (fasBlock todo tb; fasBlock todo fb)
-      | Switch (_, b, _, _) -> fasBlock todo b
-      | Loop (b, _, _, _) -> fasBlock todo b
+      | If (_, tb, fb, _, _) -> (fasBlock todo tb; fasBlock todo fb)
+      | Switch (_, b, _, _, _) -> fasBlock todo b
+      | Loop (b, _, _, _, _) -> fasBlock todo b
       | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _) -> ()
       | TryExcept _ | TryFinally _ -> E.s (E.unimp "try/except/finally")
   end
@@ -264,7 +264,7 @@ let d_cfgnodelabel () (s : stmt) =
   let label =
   begin
     match s.skind with
-      | If (e, _, _, _)  -> "if" (*sprint ~width:999 (dprintf "if %a" d_exp e)*)
+      | If (e, _, _, _, _)  -> "if" (*sprint ~width:999 (dprintf "if %a" d_exp e)*)
       | Loop _ -> "loop"
       | Break _ -> "break"
       | Continue _ -> "continue"

src/check.ml

@@ -730,11 +730,11 @@ and checkStmt (s: stmt) =
             if H.mem labels ln then
               ignore (warn "Multiply defined label %s" ln);
             H.add labels ln ()
-        | Case (e, _) ->
+        | Case (e, _, _) ->
            let t = checkExp true e in
            if not (isIntegralType t) then
                E.s (bug "Type of case expression is not integer");
-        | CaseRange (e1, e2, _) ->
+        | CaseRange (e1, e2, _, _) ->
            let t1 = checkExp true e1 in
            if not (isIntegralType t1) then
                E.s (bug "Type of case expression is not integer");
@@ -776,16 +776,18 @@ and checkStmt (s: stmt) =
           | None, _ -> ignore (warn "Invalid return value")
           | Some re', rt' -> checkExpType false re' rt'
         end
-      | Loop (b, l, _, _) -> checkBlock b
+      | Loop (b, l, el, _, _) -> checkBlock b
       | Block b -> checkBlock b
-      | If (e, bt, bf, l) ->
+      | If (e, bt, bf, l, el) ->
           currentLoc := l;
+          currentExpLoc := el;
           let te = checkExp false e in
           checkScalarType te;
           checkBlock bt;
           checkBlock bf
-      | Switch (e, b, cases, l) ->
+      | Switch (e, b, cases, l, el) ->
           currentLoc := l;
+          currentExpLoc := el;
           let t = checkExp false e in
           if not (isIntegralType t) then
               E.s (bug "Type of switch expression is not integer");
@@ -836,8 +838,9 @@ and checkInstr (i: instr) =
   if !ignoreInstr i then ()
   else
   match i with
-  | Set (dest, e, l) ->
+  | Set (dest, e, l, el) ->
       currentLoc := l;
+      currentExpLoc := el;
       let t = checkLval false false dest in
       (* Not all types can be assigned to *)
       (match unrollType t with
@@ -847,8 +850,9 @@ and checkInstr (i: instr) =
       | _ -> ());
       checkExpType false e t
 
-  | Call(dest, what, args, l) ->
+  | Call(dest, what, args, l, el) ->
       currentLoc := l;
+      currentExpLoc := el;
       let (rt, formals, isva, fnAttrs) =
         match unrollType (checkExp false what) with
           TFun(rt, formals, isva, fnAttrs) -> rt, formals, isva, fnAttrs