56 std::string _identifier,
87 using functionst = std::list<std::pair<std::regex, functiont>>;
95 using objectst = std::list<std::pair<std::regex, objectt>>;
118 if(!source.is_string())
170 if(!function.is_object())
178 if(!items.is_array())
197 split[0] ==
"ensures" ||
split[0] ==
"requires" ||
198 split[0] ==
"assigns")
200 std::ostringstream
rest;
205 else if(
split[0] ==
"assert" &&
split.size() >= 3)
207 std::ostringstream
rest;
215 (
split[2] ==
"invariant" ||
split[2] ==
"assigns" ||
216 split[2] ==
"decreases"))
218 std::ostringstream
rest;
224 else if(
split[0] ==
"stub")
226 std::ostringstream
rest;
231 else if(
split[0] ==
"remove")
233 if(
split.size() == 1)
236 if(
split[1] ==
"static")
240 "unexpected remove entry " +
split[1]);
244 "unexpected function entry " +
split[0]);
262 if(!
object.is_object())
270 if(!items.is_array())
287 if(
split[0] ==
"remove")
289 if(
split.size() == 1)
292 if(
split[1] ==
"static")
296 "unexpected remove entry " +
split[1]);
300 "unexpected object entry " +
split[0]);
322 std::vector<std::string> argv = {
"cc",
"-E",
source_file};
326 argv.push_back(
"-I");
331 argv.push_back(std::string(
"-D") +
define);
333 std::ostringstream result;
345 std::vector<std::string> argv = {
"cc",
"-E",
"-dM",
source_file};
349 argv.push_back(
"-I");
353 std::ostringstream result;
360 defines.
parse(result.str());
381 if(t.text ==
"static")
384 out << std::string(6,
' ');
410 << defines(entry.content) <<
')';
418 if(entry.clause ==
"invariant")
420 if(entry.clause ==
"assigns")
421 loop_assigns[entry.loop_type + entry.identifier] = entry.content;
422 if(entry.clause ==
"decreases")
423 loop_decreases[entry.loop_type + entry.identifier] = entry.content;
439 const auto &token = *(t++);
441 std::string invariant;
443 std::string decreases;
465 else if(token ==
"for")
484 for(; t !=
t_end; t++)
489 out <<
' ' <<
CPROVER_PREFIX <<
"assigns(" << defines(assigns) <<
')';
492 if(!invariant.empty())
495 << defines(invariant) <<
')';
498 if(!decreases.empty())
500 out <<
' ' <<
CPROVER_PREFIX <<
"decreases(" << defines(decreases)
518 if(t.text ==
"static")
521 out << std::string(6,
' ');
550 for(
const auto &entry :
config.functions)
552 if(std::regex_match(
name_opt->text, entry.first))
563 for(
const auto &entry :
config.objects)
565 if(std::regex_match(
name_opt->text, entry.first))
580 const std::string &in,
584 std::ostringstream out;
585 std::istringstream
in_str(in);
589 for(
const auto &declaration :
parsed)
static void mangle_function(const c_declarationt &declaration, const c_definest &defines, const c_wranglert::functiont &function_config, std::ostream &out)
static c_definest get_defines(const std::string &source_file, const c_wranglert &config)
static void mangle_object(const c_declarationt &declaration, const c_definest &defines, const c_wranglert::objectt &object_config, std::ostream &out)
void c_wrangler(const jsont &config)
static std::string preprocess(const std::string &source_file, const c_wranglert &c_wrangler)
static void mangle(const c_declarationt &declaration, const c_definest &defines, const c_wranglert &config, std::ostream &out)
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
This class maintains a representation of one assignment to the preprocessor macros in a C program.
void parse(const std::string &)
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Thrown when some external system fails unexpectedly.
ctokenitt match_bracket(ctokenitt t, char open, char close)
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
c_translation_unitt parse_c(std::istream &in)
int run(const std::string &what, const std::vector< std::string > &argv)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
optionalt< ctokent > declared_identifier() const
assertiont(std::string _identifier, std::string _content)
function_contract_clauset(std::string _clause, std::string _content)
std::vector< loop_contract_clauset > loop_contract
std::vector< function_contract_clauset > function_contract
std::vector< assertiont > assertions
optionalt< std::string > stub
loop_contract_clauset(std::string _loop_type, std::string _identifier, std::string _clause, std::string _content)
void configure_output(const jsont &)
void configure_objects(const jsont &)
std::vector< std::string > source_files
std::list< std::pair< std::regex, functiont > > functionst
std::list< std::pair< std::regex, objectt > > objectst
void configure_sources(const jsont &)
std::vector< std::string > includes
std::vector< std::string > defines
void configure_functions(const jsont &)