File tree Expand file tree Collapse file tree 2 files changed +7
-1
lines changed
Expand file tree Collapse file tree 2 files changed +7
-1
lines changed Original file line number Diff line number Diff line change @@ -1762,7 +1762,7 @@ struct
17621762 (* LVH.iter (fun (l, x) v ->
17631763 Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v
17641764 ) lvh; *)
1765- Marshal. output f ({name = get_string " ana.base.privatization" ; results = lvh}: result );
1765+ Marshal. output f ({name = get_string " ana.base.privatization" ^ get_string " exp.priv-prec-dump-suffix " ; results = lvh}: result );
17661766 close_out_noerr f
17671767
17681768 let finalize () =
Original file line number Diff line number Diff line change 16341634 "type" : " string" ,
16351635 "default" : " "
16361636 },
1637+ "priv-prec-dump-suffix" : {
1638+ "title" : " exp.priv-prec-dump-suffix" ,
1639+ "description" : " Suffix for name of precision dump. Useful if one has several configurations for one privatization." ,
1640+ "type" : " string" ,
1641+ "default" : " "
1642+ },
16371643 "priv-distr-init" : {
16381644 "title" : " exp.priv-distr-init" ,
16391645 "description" :
You can’t perform that action at this time.
0 commit comments