Skip to content

Commit b223d14

Browse files
Fix: sync formal parameter attributes to function type after autotuner modifies them
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/7435f504-0f43-44f3-bac5-3da617cb5cd7 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent c06e94a commit b223d14

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

src/autoTune.ml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -455,7 +455,11 @@ let apronOctagonOption factors file =
455455
set_string "ana.apron.threshold_widening_constants" "comparisons";
456456
Logs.info "Enabled octagon domain ONLY for:";
457457
Logs.info "%s" @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars;
458-
List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_relation_track",[])) info.vattr) allVars
458+
List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_relation_track",[])) info.vattr) allVars;
459+
(* Sync formal parameter attributes back to function types for correct CIL printing *)
460+
iterGlobals file (function
461+
| GFun (fd, _) -> setFormals fd fd.sformals
462+
| _ -> ())
459463
in
460464
{
461465
value = 50 * (List.length allVars) ;

0 commit comments

Comments
 (0)