Skip to content

Split goto_check #6497

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Dec 2, 2021
Merged

Split goto_check #6497

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
35ad715
split up goto_check
kroening Dec 2, 2021
2968ca9
clang-format the moved files
kroening Dec 2, 2021
7d06436
replace usage of assert()
kroening Dec 2, 2021
4f6f2a1
clean out Java-specific code from goto_check_ct
kroening Dec 2, 2021
e286cd2
clean out C/C++-specific code from goto_check_javat
kroening Dec 2, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -797,7 +797,7 @@ void janalyzer_parse_optionst::help()
HELP_SHOW_PROPERTIES
"\n"
"Program instrumentation options:\n"
HELP_GOTO_CHECK
HELP_GOTO_CHECK_JAVA
"\n"
"Other options:\n"
" --version show version and exit\n"
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ Author: Daniel Kroening, [email protected]
#include <goto-programs/show_goto_functions.h>
#include <goto-programs/show_properties.h>

#include <analyses/goto_check.h>
#include <analyses/goto_check_java.h>

#include <java_bytecode/java_bytecode_language.h>

Expand All @@ -128,7 +128,7 @@ class optionst;
"(little-endian)(big-endian)" \
OPT_SHOW_GOTO_FUNCTIONS \
OPT_SHOW_PROPERTIES \
OPT_GOTO_CHECK \
OPT_GOTO_CHECK_JAVA \
"(show-loops)" \
"(show-symbol-table)(show-parse-tree)" \
"(show-reachable-properties)(property):" \
Expand Down
6 changes: 3 additions & 3 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,8 +228,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
"self-loops-to-assumptions",
!cmdline.isset("no-self-loops-to-assumptions"));

// all checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
// all checks supported by goto_check_java
PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);

// unwind loops in java enum static initialization
if(cmdline.isset("java-unwind-enum-static"))
Expand Down Expand Up @@ -811,7 +811,7 @@ void jbmc_parse_optionst::process_goto_function(
}

// add generic checks
goto_check(
goto_check_java(
function.get_function_id(),
function.get_goto_function(),
ns,
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/jbmc/jbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]

#include <langapi/language.h>

#include <analyses/goto_check.h>
#include <analyses/goto_check_java.h>

#include <goto-checker/bmc_util.h>

Expand Down
6 changes: 3 additions & 3 deletions jbmc/src/jdiff/jdiff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
options.set_option("mm", cmdline.get_value("mm"));

// all checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);

if(cmdline.isset("debug-level"))
options.set_option("debug-level", cmdline.get_value("debug-level"));
Expand Down Expand Up @@ -278,7 +278,7 @@ bool jdiff_parse_optionst::process_goto_program(

// add generic checks
log.status() << "Generic Property Instrumentation" << messaget::eom;
goto_check(options, goto_model, ui_message_handler);
goto_check_java(options, goto_model, ui_message_handler);

// checks don't know about adjusted float expressions
adjust_float_expressions(goto_model);
Expand Down Expand Up @@ -344,7 +344,7 @@ void jdiff_parse_optionst::help()
" --compact-output output dependencies in compact mode\n"
"\n"
"Program instrumentation options:\n"
HELP_GOTO_CHECK
HELP_GOTO_CHECK_JAVA
HELP_COVER
"Java Bytecode frontend options:\n"
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/jdiff/jdiff_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Peter Schrammel
#ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
#define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H

#include <analyses/goto_check.h>
#include <analyses/goto_check_java.h>

#include <util/parse_options.h>
#include <util/timestamper.h>
Expand All @@ -29,7 +29,7 @@ class goto_modelt;
"(json-ui)" \
OPT_SHOW_GOTO_FUNCTIONS \
OPT_SHOW_PROPERTIES \
OPT_GOTO_CHECK \
OPT_GOTO_CHECK_JAVA \
OPT_COVER \
"(verbosity):(version)" \
"(no-lazy-methods)" /* should go away */ \
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ SRC = ai.cpp \
flow_insensitive_analysis.cpp \
global_may_alias.cpp \
goto_check.cpp \
goto_check_c.cpp \
goto_check_java.cpp \
goto_rw.cpp \
guard_bdd.cpp \
guard_expr.cpp \
Expand Down
Loading