Skip to content
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

Towards fixing GobView search: Avoid truncation of very large integers #1092

Merged
merged 9 commits into from
Feb 7, 2024
Merged

Towards fixing GobView search: Avoid truncation of very large integers #1092

Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
98bf2b5
avoid truncation of very large integers
stilscher Jun 19, 2023
1fa71e1
allow syntactic queries (no expression field) through Goblint
stilscher Jun 21, 2023
b6ac9e0
use negative ids for varinfos generated by Goblint and pseudo return …
stilscher Jun 22, 2023
11ab227
add test cases for syntactic and semantic search in GobView
stilscher Jun 26, 2023
2b47ef1
allow for semantic search expressions with function pointers and func…
stilscher Jun 27, 2023
c2d6c67
use function id instead of (possibly negative) hash
stilscher Jan 26, 2024
2892b8a
Merge branch 'master' into fix-gobview-search
stilscher Feb 1, 2024
7bd3b4f
add comment
stilscher Feb 1, 2024
d53037a
update GobView submodule
stilscher Feb 5, 2024
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
8 changes: 6 additions & 2 deletions src/transform/expressionEvaluation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,11 @@ struct

val global_variables =
file.globals
|> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
|> List.filter_map (function
| Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v)
| Cil.GFun (f, l) -> Some (f.svar.vname, Cil.Fv f.svar)
| Cil.GVarDecl (v, l) -> Some (v.vname, Cil.Fv v)
| _ -> None)
Comment on lines +63 to +67
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a thought for future: at some point this old expression evaluation should be switched from the odd Format-CIL parser (see goblint-cil issues) to the normal expression parser that's used for witness invariants. That avoids fixing the same issues twice.

At that point one might reconsider this being a transformation altogether, because it isn't. Simply using EvalInt or EvalValue queries directly from GobView should be possible.

val statements =
file.globals
|> List.filter_map (function Cil.GFun (f, _) -> Some f | _ -> None)
Expand All @@ -77,7 +81,7 @@ struct
(* Compute the available local variables *)
let local_variables =
match Hashtbl.find_option statements location with
| Some (function_definition, _) -> function_definition.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
| Some (fd, _) -> fd.slocals @ fd.sformals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
| None -> []
in
(* Parse expression *)
Expand Down