Skip to content

Commit 8bf62ad

Browse files
committed
Add GOTO_HARNESS_PREFIX.
Before this change, we were using CPROVER_PREFIX, which was causing some symbols to be dropped before the C code output because of the prefix symbolising CProver internal values.
1 parent a76122d commit 8bf62ad

File tree

2 files changed

+7
-6
lines changed

2 files changed

+7
-6
lines changed

src/goto-harness/recursive_initialization.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -479,10 +479,10 @@ static symbolt &get_fresh_global_symbol(
479479
irep_idt mode)
480480
{
481481
source_locationt source_location{};
482-
source_location.set_file(CPROVER_PREFIX "harness.c");
482+
source_location.set_file(GOTO_HARNESS_PREFIX "harness.c");
483483
symbolt &fresh_symbol = get_fresh_aux_symbol(
484484
std::move(symbol_type),
485-
CPROVER_PREFIX,
485+
GOTO_HARNESS_PREFIX,
486486
symbol_base_name,
487487
source_locationt{},
488488
mode,
@@ -494,7 +494,7 @@ static symbolt &get_fresh_global_symbol(
494494
fresh_symbol.is_file_local = false;
495495
fresh_symbol.is_thread_local = false;
496496
fresh_symbol.is_state_var = false;
497-
fresh_symbol.module = CPROVER_PREFIX "harness";
497+
fresh_symbol.module = GOTO_HARNESS_PREFIX "harness";
498498
fresh_symbol.location = std::move(source_location);
499499
return fresh_symbol;
500500
}
@@ -529,7 +529,7 @@ symbol_exprt recursive_initializationt::get_fresh_local_symexpr(
529529
{
530530
symbolt &fresh_symbol = get_fresh_aux_symbol(
531531
signed_int_type(),
532-
CPROVER_PREFIX,
532+
GOTO_HARNESS_PREFIX,
533533
symbol_name,
534534
source_locationt{},
535535
initialization_config.mode,
@@ -545,7 +545,7 @@ symbol_exprt recursive_initializationt::get_fresh_local_typed_symexpr(
545545
{
546546
symbolt &fresh_symbol = get_fresh_aux_symbol(
547547
type,
548-
CPROVER_PREFIX,
548+
GOTO_HARNESS_PREFIX,
549549
symbol_name,
550550
source_locationt{},
551551
initialization_config.mode,
@@ -583,7 +583,7 @@ symbolt &recursive_initializationt::get_fresh_param_symbol(
583583
{
584584
symbolt &param_symbol = get_fresh_aux_symbol(
585585
symbol_type,
586-
CPROVER_PREFIX,
586+
GOTO_HARNESS_PREFIX,
587587
symbol_name,
588588
source_locationt{},
589589
initialization_config.mode,

src/goto-harness/recursive_initialization.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Diffblue Ltd.
2222
#include "function_harness_generator_options.h"
2323
#include "goto_harness_generator.h"
2424

25+
#define GOTO_HARNESS_PREFIX "GOTO_HARNESS"
2526
struct recursive_initialization_configt
2627
{
2728
std::size_t min_null_tree_depth = 1;

0 commit comments

Comments
 (0)