Skip to content

Commit 76f2064

Browse files
WIP add additional regression tests
1 parent 596683d commit 76f2064

File tree

6 files changed

+52
-12
lines changed

6 files changed

+52
-12
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
3+
void change_pointer_target_of_const_pointer(
4+
int *const constant_pointer_to_nonconst);
5+
6+
int main(void)
7+
{
8+
int x = 10;
9+
change_pointer_target_of_const_pointer(&x);
10+
assert(x == 10);
11+
return 0;
12+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--replace-function-body change_pointer_target_of_const_pointer --replace-function-body-options havoc,params:.*
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] assertion x == 10: FAILURE$
7+
--
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
void change_target_of_pointer_to_pointer_to_const(
4+
const int **pointer_to_pointer_to_const);
5+
6+
int main(void)
7+
{
8+
int x = 10;
9+
int *px = &x;
10+
assert(*px == 10);
11+
change_target_of_pointer_to_pointer_to_const(&px);
12+
assert(x == 10);
13+
assert(*px == 10);
14+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--replace-function-body change_target_of_pointer_to_pointer_to_const --replace-function-body-options havoc,params:.*
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] assertion \*px == 10: SUCCESS$
7+
^\[main.assertion.2\] assertion x == 10: SUCCESS$
8+
^\[main.assertion.3\] assertion \*px == 10: FAILURE$
9+
--

src/goto-programs/replace_function_bodies.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -70,8 +70,8 @@ class assume_false_replace_function_bodiest : public replace_function_bodiest
7070
const irep_idt &function_name) override
7171
{
7272
auto const &function_symbol = symbol_table.lookup_ref(function_name);
73-
auto add_instruction = [&]()
74-
{
73+
// NOLINTNEXTLINE
74+
auto add_instruction = [&]() {
7575
auto instruction = function.body.add_instruction();
7676
instruction->function = function_name;
7777
instruction->source_location = function_symbol.location;
@@ -93,8 +93,8 @@ class assert_false_replace_function_bodiest : public replace_function_bodiest
9393
const irep_idt &function_name) override
9494
{
9595
auto const &function_symbol = symbol_table.lookup_ref(function_name);
96-
auto add_instruction = [&]()
97-
{
96+
// NOLINTNEXTLINE
97+
auto add_instruction = [&]() {
9898
auto instruction = function.body.add_instruction();
9999
instruction->function = function_name;
100100
instruction->source_location = function_symbol.location;
@@ -124,8 +124,8 @@ class assert_false_then_assume_false_replace_function_bodiest
124124
const irep_idt &function_name) override
125125
{
126126
auto const &function_symbol = symbol_table.lookup_ref(function_name);
127-
auto add_instruction = [&]()
128-
{
127+
// NOLINTNEXTLINE
128+
auto add_instruction = [&]() {
129129
auto instruction = function.body.add_instruction();
130130
instruction->function = function_name;
131131
instruction->source_location = function_symbol.location;
@@ -178,8 +178,8 @@ class havoc_replace_function_bodiest : public replace_function_bodiest
178178
const irep_idt &function_name) override
179179
{
180180
auto const &function_symbol = symbol_table.lookup_ref(function_name);
181-
auto add_instruction = [&]()
182-
{
181+
// NOLINTNEXTLINE
182+
auto add_instruction = [&]() {
183183
auto instruction = function.body.add_instruction();
184184
instruction->function = function_name;
185185
instruction->source_location = function_symbol.location;
@@ -241,8 +241,7 @@ class havoc_replace_function_bodiest : public replace_function_bodiest
241241
class replace_function_bodies_errort : public std::runtime_error
242242
{
243243
public:
244-
explicit replace_function_bodies_errort(
245-
const std::string &reason)
244+
explicit replace_function_bodies_errort(const std::string &reason)
246245
: runtime_error(reason)
247246
{
248247
}

src/goto-programs/replace_function_bodies.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,7 @@ Author: DiffBlue Ltd.
1010
#define CPROVER_GOTO_PROGRAMS_REPLACE_FUNCTION_BODIES_H
1111

1212
#include <regex>
13-
#include <vector>
14-
#include <iostream>
13+
#include <memory>
1514

1615
#include <goto-programs/goto_functions.h>
1716
#include <util/std_code.h>

0 commit comments

Comments
 (0)