Skip to content

Commit 1d021aa

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#4666 from tautschnig/suppression-fix
Make sure pragmas propagate to all source locations
2 parents 9f06b86 + 1b7b347 commit 1d021aa

File tree

10 files changed

+80
-90
lines changed

10 files changed

+80
-90
lines changed

‎regression/cbmc/pragma_cprover2/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@ int foo(int x)
55

66
int main()
77
{
8-
int n;
8+
int m, n;
99

1010
#pragma CPROVER check push
1111
#pragma CPROVER check disable "signed-overflow"
1212
// do not generate assertions for the following statements
13-
int x = n + n;
13+
int x = m = n + n;
1414
++n;
1515
n++;
1616
n += 1;

‎src/analyses/goto_check.cpp

Lines changed: 24 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ Author: Daniel Kroening, [email protected]
2929
#include <util/simplify_expr.h>
3030
#include <util/std_expr.h>
3131
#include <util/std_types.h>
32-
#include <util/string_utils.h>
3332

3433
#include <langapi/language.h>
3534
#include <langapi/mode.h>
@@ -1805,35 +1804,31 @@ void goto_checkt::goto_check(
18051804
goto_programt::instructiont &i=*it;
18061805

18071806
flag_resett flag_resetter;
1808-
if(!i.source_location.get_comment().empty())
1807+
const auto &pragmas = i.source_location.get_pragmas();
1808+
for(const auto &d : pragmas)
18091809
{
1810-
auto disabled_checks = split_string(
1811-
id2string(i.source_location.get_comment()), ',', true, true);
1812-
for(const auto &d : disabled_checks)
1813-
{
1814-
if(d == "disable:bounds-check")
1815-
flag_resetter.set_flag(enable_bounds_check, false);
1816-
else if(d == "disable:pointer-check")
1817-
flag_resetter.set_flag(enable_pointer_check, false);
1818-
else if(d == "disable:memory-leak-check")
1819-
flag_resetter.set_flag(enable_memory_leak_check, false);
1820-
else if(d == "disable:div-by-zero-check")
1821-
flag_resetter.set_flag(enable_div_by_zero_check, false);
1822-
else if(d == "disable:signed-overflow-check")
1823-
flag_resetter.set_flag(enable_signed_overflow_check, false);
1824-
else if(d == "disable:unsigned-overflow-check")
1825-
flag_resetter.set_flag(enable_unsigned_overflow_check, false);
1826-
else if(d == "disable:pointer-overflow-check")
1827-
flag_resetter.set_flag(enable_pointer_overflow_check, false);
1828-
else if(d == "disable:float-overflow-check")
1829-
flag_resetter.set_flag(enable_float_overflow_check, false);
1830-
else if(d == "disable:conversion-check")
1831-
flag_resetter.set_flag(enable_conversion_check, false);
1832-
else if(d == "disable:undefined-shift-check")
1833-
flag_resetter.set_flag(enable_undefined_shift_check, false);
1834-
else if(d == "disable:nan-check")
1835-
flag_resetter.set_flag(enable_nan_check, false);
1836-
}
1810+
if(d.first == "disable:bounds-check")
1811+
flag_resetter.set_flag(enable_bounds_check, false);
1812+
else if(d.first == "disable:pointer-check")
1813+
flag_resetter.set_flag(enable_pointer_check, false);
1814+
else if(d.first == "disable:memory-leak-check")
1815+
flag_resetter.set_flag(enable_memory_leak_check, false);
1816+
else if(d.first == "disable:div-by-zero-check")
1817+
flag_resetter.set_flag(enable_div_by_zero_check, false);
1818+
else if(d.first == "disable:signed-overflow-check")
1819+
flag_resetter.set_flag(enable_signed_overflow_check, false);
1820+
else if(d.first == "disable:unsigned-overflow-check")
1821+
flag_resetter.set_flag(enable_unsigned_overflow_check, false);
1822+
else if(d.first == "disable:pointer-overflow-check")
1823+
flag_resetter.set_flag(enable_pointer_overflow_check, false);
1824+
else if(d.first == "disable:float-overflow-check")
1825+
flag_resetter.set_flag(enable_float_overflow_check, false);
1826+
else if(d.first == "disable:conversion-check")
1827+
flag_resetter.set_flag(enable_conversion_check, false);
1828+
else if(d.first == "disable:undefined-shift-check")
1829+
flag_resetter.set_flag(enable_undefined_shift_check, false);
1830+
else if(d.first == "disable:nan-check")
1831+
flag_resetter.set_flag(enable_nan_check, false);
18371832
}
18381833

18391834
new_code.clear();

‎src/ansi-c/ansi_c_parser.h

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#define CPROVER_ANSI_C_ANSI_C_PARSER_H
1212

1313
#include <cassert>
14+
#include <set>
1415

1516
#include <util/parser.h>
1617
#include <util/expr.h>
@@ -69,7 +70,7 @@ class ansi_c_parsert:public parsert
6970
unsigned parenthesis_counter;
7071
std::string string_literal;
7172
std::list<exprt> pragma_pack;
72-
std::list<irep_idt> pragma_cprover;
73+
std::list<std::set<irep_idt>> pragma_cprover;
7374

7475
typedef configt::ansi_ct::flavourt modet;
7576
modet mode;
@@ -145,6 +146,16 @@ class ansi_c_parsert:public parsert
145146
lookup(base_name, identifier, false, true);
146147
return identifier;
147148
}
149+
150+
void set_pragma_cprover()
151+
{
152+
source_location.remove(ID_pragma);
153+
for(const auto &pragma_set : pragma_cprover)
154+
{
155+
for(const auto &pragma : pragma_set)
156+
source_location.add_pragma(pragma);
157+
}
158+
}
148159
};
149160

150161
extern ansi_c_parsert ansi_c_parser;

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -243,16 +243,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)
243243
}
244244

245245
ansi_c_declarationt declaration;
246-
irep_idt comment = code.source_location().get_comment();
247246
declaration.swap(code.op0());
248-
if(!comment.empty())
249-
{
250-
for(auto &d : declaration.declarators())
251-
{
252-
if(d.source_location().get_comment().empty())
253-
d.add_source_location().set_comment(comment);
254-
}
255-
}
256247

257248
if(declaration.get_is_static_assert())
258249
{

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2019,10 +2019,6 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
20192019
throw 0;
20202020
}
20212021

2022-
irep_idt comment = expr.source_location().get_comment();
2023-
if(!comment.empty() && f_op.source_location().get_comment().empty())
2024-
f_op.add_source_location().set_comment(comment);
2025-
20262022
const code_typet &code_type=to_code_type(f_op.type());
20272023

20282024
expr.type()=code_type.return_type();

‎src/ansi-c/expr2c.cpp

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
2727
#include <util/pointer_predicates.h>
2828
#include <util/prefix.h>
2929
#include <util/string_constant.h>
30+
#include <util/string_utils.h>
3031
#include <util/suffix.h>
3132
#include <util/symbol.h>
3233

@@ -2796,11 +2797,31 @@ std::string expr2ct::convert_code(
27962797
{
27972798
static bool comment_done=false;
27982799

2799-
if(!comment_done && !src.source_location().get_comment().empty())
2800+
if(
2801+
!comment_done && (!src.source_location().get_comment().empty() ||
2802+
!src.source_location().get_pragmas().empty()))
28002803
{
28012804
comment_done=true;
2802-
std::string dest=indent_str(indent);
2803-
dest+="/* "+id2string(src.source_location().get_comment())+" */\n";
2805+
std::string dest;
2806+
if(!src.source_location().get_comment().empty())
2807+
{
2808+
dest += indent_str(indent);
2809+
dest += "/* " + id2string(src.source_location().get_comment()) + " */\n";
2810+
}
2811+
if(!src.source_location().get_pragmas().empty())
2812+
{
2813+
std::ostringstream oss;
2814+
oss << indent_str(indent) << "/* ";
2815+
const auto &pragmas = src.source_location().get_pragmas();
2816+
join_strings(
2817+
oss,
2818+
pragmas.begin(),
2819+
pragmas.end(),
2820+
',',
2821+
[](const std::pair<irep_idt, irept> &p) { return p.first; });
2822+
oss << " */\n";
2823+
dest += oss.str();
2824+
}
28042825
dest+=convert_code(src, indent);
28052826
comment_done=false;
28062827
return dest;

‎src/ansi-c/parser.y

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,6 @@ extern char *yyansi_ctext;
2424

2525
#include "literals/convert_integer_literal.h"
2626

27-
#include <util/string_utils.h>
28-
29-
#include <sstream>
30-
3127
#include "ansi_c_y.tab.h"
3228

3329
#ifdef _MSC_VER
@@ -2310,38 +2306,10 @@ statement_list:
23102306
statement
23112307
{
23122308
init($$);
2313-
if(!PARSER.pragma_cprover.empty())
2314-
{
2315-
std::ostringstream oss;
2316-
join_strings(
2317-
oss,
2318-
PARSER.pragma_cprover.begin(),
2319-
PARSER.pragma_cprover.end(),
2320-
',');
2321-
parser_stack($1).add_source_location().set_comment(oss.str());
2322-
Forall_operands(it, parser_stack($1))
2323-
{
2324-
it->add_source_location().set_comment(oss.str());
2325-
}
2326-
}
23272309
mto($$, $1);
23282310
}
23292311
| statement_list statement
23302312
{
2331-
if(!PARSER.pragma_cprover.empty())
2332-
{
2333-
std::ostringstream oss;
2334-
join_strings(
2335-
oss,
2336-
PARSER.pragma_cprover.begin(),
2337-
PARSER.pragma_cprover.end(),
2338-
',');
2339-
parser_stack($2).add_source_location().set_comment(oss.str());
2340-
Forall_operands(it, parser_stack($2))
2341-
{
2342-
it->add_source_location().set_comment(oss.str());
2343-
}
2344-
}
23452313
mto($$, $2);
23462314
}
23472315
;

‎src/ansi-c/scanner.l

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -402,11 +402,14 @@ void ansi_c_scanner_init()
402402

403403
/* CProver specific pragmas: hint to disable named checks */
404404
<CPROVER_PRAGMA>{ws}"check"{ws}"push" {
405-
PARSER.pragma_cprover.push_back(irep_idt{});
405+
PARSER.pragma_cprover.push_back({});
406406
}
407407
<CPROVER_PRAGMA>{ws}"check"{ws}"pop" {
408408
if(!PARSER.pragma_cprover.empty())
409+
{
409410
PARSER.pragma_cprover.pop_back();
411+
PARSER.set_pragma_cprover();
412+
}
410413
}
411414
<CPROVER_PRAGMA>{ws}"check"{ws}"disable"{ws}{named_check} {
412415
std::string tmp(yytext);
@@ -416,16 +419,10 @@ void ansi_c_scanner_init()
416419
std::string(tmp, p, tmp.size() - p - 1) +
417420
std::string("-check");
418421
if(PARSER.pragma_cprover.empty())
419-
PARSER.pragma_cprover.push_back(value);
422+
PARSER.pragma_cprover.push_back({value});
420423
else
421-
{
422-
if(!PARSER.pragma_cprover.back().empty())
423-
{
424-
value =
425-
id2string(PARSER.pragma_cprover.back()) + "," + value;
426-
}
427-
PARSER.pragma_cprover.back() = value;
428-
}
424+
PARSER.pragma_cprover.back().insert(value);
425+
PARSER.set_pragma_cprover();
429426
}
430427

431428
<CPROVER_PRAGMA>. {

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -724,6 +724,7 @@ IREP_ID_ONE(clear_may)
724724
IREP_ID_ONE(get_must)
725725
IREP_ID_ONE(set_must)
726726
IREP_ID_ONE(clear_must)
727+
IREP_ID_ONE(pragma)
727728

728729
// Projects depending on this code base that wish to extend the list of
729730
// available ids should provide a file local_irep_ids.def in their source tree

‎src/util/source_location.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,16 @@ class source_locationt:public irept
192192

193193
optionalt<std::string> full_path() const;
194194

195+
void add_pragma(const irep_idt &pragma)
196+
{
197+
add(ID_pragma).add(pragma);
198+
}
199+
200+
const irept::named_subt &get_pragmas() const
201+
{
202+
return find(ID_pragma).get_named_sub();
203+
}
204+
195205
protected:
196206
std::string as_string(bool print_cwd) const;
197207
};

0 commit comments

Comments
 (0)