8000 Add end locations to statements by sim642 · Pull Request #51 · goblint/cil · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Add end locations to statements #51

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 19 commits into from
Nov 23, 2021
Merged

Add end locations to statements #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
9dbaf0b
Add location end fields to Cabs location
sim642 Nov 15, 2021
d304524
Add location end fields to Cil location
sim642 Nov 15, 2021
1658e1d
Add location joining for simple statements
sim642 Nov 15, 2021
d0cbef3
Add enough joined locations for Goblint regression suite output
sim642 Nov 16, 2021
65112de
Add remaining statement joined locations
sim642 Nov 16, 2021
416c48b
Document Cil.location end fields
sim642 Nov 16, 2021
0e16400
Add location end comparison
sim642 Nov 16, 2021
43a092c
Deduplicate unknown location definitions
sim642 Nov 16, 2021
2114881
Add expression locations to ifs
sim642 Nov 18, 2021
be9f7b2
Add expression locations to whiles
sim642 Nov 18, 2021
6766d26
Add expression locations to do-whiles
sim642 Nov 18, 2021
91ab0f3
Add expression locations to fors
sim642 Nov 18, 2021
42c3744
Add expression locations to switches
sim642 Nov 18, 2021
e117797
Add expression locations to instructions
sim642 Nov 19, 2021
25f0c6f
Fix Set in longBlock test
sim642 Nov 19, 2021
5f099de
Unify convLoc style in Cabs2cil.doDecl
sim642 Nov 22, 2021
0ed7711
Extend comments about registerLabelsVisitor not touching currentExpLoc
sim642 Nov 22, 2021
f1e59f6
Merge branch 'develop' into loc-end
sim642 Nov 23, 2021
c3ef49d
Add end locations to CHANGES
sim642 Nov 23, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions CHANGES
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
24 changes: 12 additions & 12 deletions src/cfg.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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;
Expand All @@ -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 *)
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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"
Expand Down
18 changes: 11 additions & 7 deletions src/check.ml
View file
Open in desktop
6DB6
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
Loading
0