cil-project / cil

C Intermediate Language
Other
348 stars 86 forks source link

Syntactic search does not find variable occurence #54

Closed stilscher closed 1 year ago

stilscher commented 1 year ago

Syntactic search returns no results (not when querying through GobView, but also not when querying through Goblint directly).

Steps to reproduce the issue:

Run the Goblint-http server:

./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set save_run run -v --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"

Open the web UI. Scroll down until you see "Switch to JSON editor" and click it. Enter the following query and click "Execute":

{"kind":["var"],"target":["name","fail"],"find":["uses"],"expression":"","mode":["Must"]}

If you allow for non-semantic queries in the expression evaluator (expressionEvaluation.ml) in Goblint[^1] the query can also directly be handed to Goblint. Save the same query in a file (e.g., query.json) and execute the syntactic search in the terminal like this: ./goblint --set trans.activated[+] expeval -v --set trans.expeval.query_file_name query.json tests/regression/00-sanity/01-assert.c

This also does not return any result.

[^1]: This can for example be quickly hacked by changing https://github.com/goblint/analyzer/blob/5464235e9cc77156746da5f25d336f9d9dac0d1e/src/transform/expressionEvaluation.ml#L195 to |> (fun ls -> if query.expression != "" then List.map (fun (n, l, s, i) -> ((n, l, s, i), evaluator#evaluate l query.expression)) ls else List.map (fun a -> (a, None)) ls)

stilscher commented 1 year ago

Sorry, I confused this repository with our fork.