Skip to content

Commit 7d5372d

Browse files
sipmasipma
committed
CHC: fix for regression-test failure
1 parent 07b782c commit 7d5372d

File tree

11 files changed

+130
-71
lines changed

11 files changed

+130
-71
lines changed

‎CodeHawk/CHC/cchanalyze/cCHAnalyze.ml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ let analyze_procedure_with_intervals (proc:procedure_int) (system:system_int)
7676
analysis_setup#addDomain intervals_domain (new intervals_domain_no_arrays_t);
7777
analysis_setup#setOpSemantics (semantics intervals_domain);
7878
analysis_setup#analyze_procedure system proc;
79-
log_info "Interval analysis completed"
79+
log_info "Interval analysis completed [%s:%d]" __FILE__ __LINE__
8080
end
8181

8282

@@ -93,7 +93,7 @@ let analyze_procedure_with_pepr
9393
pepr_domain (mk_pepr_domain_no_arrays params timeout);
9494
analysis_setup#setOpSemantics (semantics pepr_domain);
9595
analysis_setup#analyze_procedure system proc;
96-
log_info "Pepr analysis completed"
96+
log_info "Pepr analysis completed [%s:%d]" __FILE__ __LINE__
9797
end
9898

9999

@@ -105,7 +105,7 @@ let analyze_procedure_with_valuesets (proc:procedure_int) (system:system_int)
105105
analysis_setup#addDomain valueset_domain (new valueset_domain_no_arrays_t);
106106
analysis_setup#setOpSemantics (semantics valueset_domain);
107107
analysis_setup#analyze_procedure system proc;
108-
log_info "Value set analysis completed"
108+
log_info "Value set analysis completed [%s:%d]" __FILE__ __LINE__
109109
end
110110

111111

@@ -120,7 +120,7 @@ let analyze_procedure_with_linear_equalities
120120
linear_equalities_domain (new linear_equalities_domain_no_arrays_t);
121121
analysis_setup#setOpSemantics (semantics linear_equalities_domain);
122122
analysis_setup#analyze_procedure system proc;
123-
log_info "Linear equality analysis completed"
123+
log_info "Linear equality analysis completed [%s:%d]" __FILE__ __LINE__
124124
end
125125
with
126126
| CHFailure p ->
@@ -142,7 +142,7 @@ let analyze_procedure_with_symbolic_sets (proc:procedure_int) (system:system_int
142142
symbolic_sets_domain (new symbolic_sets_domain_no_arrays_t);
143143
analysis_setup#setOpSemantics (semantics symbolic_sets_domain);
144144
analysis_setup#analyze_procedure system proc;
145-
log_info "symbolic sets analysis completed"
145+
log_info "symbolic sets analysis completed [%s:%d]" __FILE__ __LINE__
146146
end
147147

148148

@@ -173,7 +173,7 @@ let analyze_procedure_with_sym_pointersets
173173
sym_pointersets_domain (new timed_symbolic_sets_domain_no_arrays_t timeout);
174174
analysis_setup#setOpSemantics (semantics sym_pointersets_domain);
175175
analysis_setup#analyze_procedure system proc;
176-
log_info "symbolic pointerset analysis completed"
176+
log_info "symbolic pointerset analysis completed [%s:%d]" __FILE__ __LINE__
177177
end
178178

179179

‎CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ let make_invariant_generation_spec t =
162162
let process_function gspecs fname =
163163
try
164164
if !function_to_be_analyzed = fname || !function_to_be_analyzed = "" then
165-
let _ = log_info "analyze function %s" fname in
165+
let _ = log_info "analyze function %s [%s:%d]" fname __FILE__ __LINE__ in
166166
let fundec = read_function_semantics fname in
167167
let fdecls = fundec.sdecls in
168168
let _ = read_proof_files fname fdecls in
@@ -175,9 +175,10 @@ let process_function gspecs fname =
175175
let openpos = List.filter (fun po -> not po#is_closed) proofObligations in
176176
let _ =
177177
log_info
178-
"Obtained %d proof obligation(s) of which %d open"
178+
"Obtained %d proof obligation(s) of which %d open [%s:%d]"
179179
(List.length proofObligations)
180-
(List.length openpos) in
180+
(List.length openpos)
181+
__FILE__ __LINE__ in
181182
if (List.length openpos) > 0 then
182183
let callcount = proof_scaffolding#get_call_count fname in
183184
let _ =
@@ -286,7 +287,7 @@ let process_function gspecs fname =
286287
let env = mk_c_environment fundec varmgr in
287288
begin
288289
check_proof_obligations env fnApi invio proofObligations;
289-
log_info "checked proof obligations";
290+
log_info "checked proof obligations [%s:%d]" __FILE__ __LINE__;
290291
save_invs fname invio;
291292
save_vars fname varmgr;
292293
save_proof_files fname;
@@ -350,16 +351,18 @@ let generate_and_check_process_file (domains: string list) =
350351
let _ = read_cfile_assignment_dictionary () in
351352
let _ = read_cfile_contract () in
352353
let _ = file_contract#collect_file_attributes in
353-
let _ = log_info "Read file-level xml files" in
354+
let _ = log_info "Read file-level xml files [%s:%d]" __FILE__ __LINE__ in
354355
let functions = fenv#get_application_functions in
355-
let _ = log_info "Processing %d functions" (List.length functions) in
356+
let _ =
357+
log_info "Processing %d functions [%s:%d]"
358+
(List.length functions) __FILE__ __LINE__ in
356359
let _ = List.iter (fun f -> process_function gspecs f.vname) functions in
357360
let _ = save_cfile_assignment_dictionary () in
358361
let _ = save_cfile_dictionary () in
359362
let _ = save_cfile_context () in
360363
let _ = save_cfile_interface_dictionary () in
361364
let _ = save_cfile_predicate_dictionary () in
362-
let _ = log_info "Saved file-level xml files" in
365+
let _ = log_info "Saved file-level xml files [%s:%d]" __FILE__ __LINE__ in
363366
()
364367
with
365368
| CHXmlReader.IllFormed ->

‎CodeHawk/CHC/cchcil/cCHXParseFile.ml‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,9 @@ let check_targetdirectory () =
8686
if !targetdirectory = "" then
8787
begin
8888
log_warning
89-
"Target directory not set: using current directory as target directory";
89+
("Target directory not set: using current directory as target "
90+
^^ "directory [%s:%d]")
91+
__FILE__ __LINE__;
9092
targetdirectory := Sys.getcwd ()
9193
end
9294

@@ -114,7 +116,9 @@ let sanitize_targetfilename name =
114116
let newname =
115117
(String.sub name 0 (spos2+1))
116118
^ (String.sub name (pos+2) ((String.length name) - (pos+2))) in
117-
let _ = log_info "Change name from %s into %s" name newname in
119+
let _ =
120+
log_info "Change name from %s into %s [%s:%d]"
121+
name newname __FILE__ __LINE__ in
118122
newname
119123
with
120124
Not_found -> name
@@ -222,7 +226,7 @@ let cil_function_to_file target (f: fundec) (dir: string) =
222226
write_xml_function_definition functionNode f target;
223227
root#appendChildren [functionNode];
224228
file_output#saveFile ffilename doc#toPretty;
225-
log_info "Saved function file %s" ffilename
229+
log_info "Saved function file %s [%s:%d]" ffilename __FILE__ __LINE__
226230
end
227231

228232

‎CodeHawk/CHC/cchcil/cHCilDeclarations.ml‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -124,9 +124,10 @@ object (self)
124124
| Error e ->
125125
begin
126126
log_error
127-
"index_varinfo: %s; %s"
127+
"index_varinfo: %s; %s [%s:%d]"
128128
vinfo.vname
129-
(String.concat ", " e);
129+
(String.concat ", " e)
130+
__FILE__ __LINE__;
130131
raise
131132
(CHFailure
132133
(LBLOCK [
@@ -152,9 +153,10 @@ object (self)
152153
| Error e ->
153154
begin
154155
log_error
155-
"index fieldinfo: %s %s"
156+
"index fieldinfo: %s %s [%s:%d]"
156157
finfo.fname
157-
(String.concat ", " e);
158+
(String.concat ", " e)
159+
__FILE__ __LINE__;
158160
raise
159161
(CHFailure
160162
(LBLOCK [
@@ -183,9 +185,10 @@ object (self)
183185
| Error e ->
184186
begin
185187
log_error
186-
"index enumitem: %s %s"
188+
"index enumitem: %s %s [%s:%d]"
187189
name
188-
(String.concat ", " e);
190+
(String.concat ", " e)
191+
__FILE__ __LINE__;
189192
raise
190193
(CHFailure
191194
(LBLOCK [

‎CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -172,35 +172,42 @@ let main () =
172172
else if !cmd = "primary" then
173173
begin
174174
primary_process_file ();
175-
log_info "primary proof obligations generated";
175+
log_info "primary proof obligations generated [%s:%d]" __FILE__ __LINE__;
176176
save_log_files "primary";
177-
log_info "primary proof obligations log files saved"
177+
log_info
178+
"primary proof obligations log files saved [%s:%d]" __FILE__ __LINE__
178179
end
179180

180181
else if !cmd = "localinvs" then
181182
begin
182183
invariants_process_file (List.rev !domains);
183-
log_info "Local invariants generated";
184+
log_info "Local invariants generated [%s:%d]" __FILE__ __LINE__;
184185
save_log_files "localinvs";
185-
log_info "Local invariant generation log files saved"
186+
log_info
187+
"Local invariant generation log files saved [%s:%d]" __FILE__ __LINE__
186188
end
187189

188190
else if !cmd = "globalinvs" then ()
189191

190192
else if !cmd = "check" then
191193
begin
192194
check_process_file ();
193-
log_info "Proof obligations checked";
195+
log_info "Proof obligations checked [%s:%d" __FILE__ __LINE__;
194196
save_log_files "check";
195-
log_info "Proof obligation checking log files saved"
197+
log_info
198+
"Proof obligation checking log files saved [%s:%d]" __FILE__ __LINE__
196199
end
197200

198201
else if !cmd = "generate_and_check" then
199202
begin
200203
generate_and_check_process_file (List.rev !domains);
201-
log_info "Invariants generated and proof obligations checked";
204+
log_info
205+
"Invariants generated and proof obligations checked [%s:%d]"
206+
__FILE__ __LINE__;
202207
save_log_files "gencheck";
203-
log_info "Invariant generation and proof obligation check log files saved"
208+
log_info
209+
"Invariant generation and proof obligation check log files saved [%s:%d]"
210+
__FILE__ __LINE__
204211
end
205212

206213
else

‎CodeHawk/CHC/cchlib/cCHCAttributes.ml‎

Lines changed: 24 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,11 @@ let convert_attribute_to_function_conditions
6262
| _ ->
6363
begin
6464
log_info
65-
"attribute conversion for %s: attribute parameters %s not recognized"
65+
("attribute conversion for %s: attribute parameters %s not "
66+
^^ "recognized [%s:%d]")
6667
name
67-
(String.concat ", " (List.map attrparam_to_string attrparams));
68+
(String.concat ", " (List.map attrparam_to_string attrparams))
69+
__FILE__ __LINE__;
6870
([], [])
6971
end) in
7072

@@ -83,9 +85,11 @@ let convert_attribute_to_function_conditions
8385
| _ ->
8486
begin
8587
log_info
86-
"attribute conversion for %s: attribute parameters %s not recognized"
88+
("attribute conversion for %s: attribute parameters %s not "
89+
^^ "recognized [%s:%d]")
8790
name
88-
(String.concat ", " (List.map attrparam_to_string attrparams));
91+
(String.concat ", " (List.map attrparam_to_string attrparams))
92+
__FILE__ __LINE__;
8993
[]
9094
end) in
9195
(pre, [], [])
@@ -102,9 +106,11 @@ let convert_attribute_to_function_conditions
102106
| _ ->
103107
begin
104108
log_info
105-
"attribute conversion for %s: attribute parameters %s not recognized"
109+
("attribute conversion for %s: attribute parameters %s not "
110+
^^ "recognized [%s:%d]")
106111
name
107-
(String.concat ", " (List.map attrparam_to_string attrparams));
112+
(String.concat ", " (List.map attrparam_to_string attrparams))
113+
__FILE__ __LINE__;
108114
[]
109115
end) in
110116
([], post, [])
@@ -118,9 +124,10 @@ let convert_attribute_to_function_conditions
118124
begin
119125
log_info
120126
("attribute conversion for %s: parameter %s not recognized "
121-
^^ "(excluded)")
127+
^^ "(excluded) [%s:%d]")
122128
name
123-
(attrparam_to_string attrparam);
129+
(attrparam_to_string attrparam)
130+
__FILE__ __LINE__;
124131
acc
125132
end) [] attrparams in
126133
(pre, [], [])
@@ -137,9 +144,10 @@ let convert_attribute_to_function_conditions
137144
begin
138145
log_info
139146
("attribute conversion for %s: parameter %s not recognized "
140-
^^ "(excluded)")
147+
^^ "(excluded) [%s:%d]")
141148
name
142-
(attrparam_to_string attrparam);
149+
(attrparam_to_string attrparam)
150+
__FILE__ __LINE__;
143151
acc
144152
end) [] attrparams in
145153
(pre, [], [])
@@ -165,9 +173,10 @@ let convert_attribute_to_function_conditions
165173
begin
166174
log_info
167175
("attribute conversion for %s: parameter %s not recognized "
168-
^^ "(excluded)")
176+
^^ "(excluded) [%s:%d]")
169177
name
170-
(attrparam_to_string attrparam);
178+
(attrparam_to_string attrparam)
179+
__FILE__ __LINE__;
171180
acc
172181
end) [] attrparams in
173182
([], [], se)
@@ -188,8 +197,10 @@ let attribute_update_globalvar_contract
188197
| Attr ("chkc_not_null", []) -> gvarc#set_not_null
189198
| Attr (s, attrparams) ->
190199
log_info
191-
"global variable attribute %s for %s with %d parameters not recognized"
200+
("global variable attribute %s for %s with %d parameters not "
201+
^^ "recognized [%s:%d]")
192202
s
193203
gvarc#get_name
194204
(List.length attrparams)
205+
__FILE__ __LINE__
195206

0 commit comments

Comments
 (0)