34#include <unordered_map>
61 std::string _identifier,
90 using functionst = std::list<std::pair<std::regex, functiont>>;
98 using objectst = std::list<std::pair<std::regex, objectt>>;
121 if(!source.is_string())
173 if(!function.is_object())
181 if(!items.is_array())
200 split[0] ==
"ensures" ||
split[0] ==
"requires" ||
201 split[0] ==
"assigns")
203 std::ostringstream
rest;
208 else if(
split[0] ==
"assert" &&
split.size() >= 3)
210 std::ostringstream
rest;
219 std::ostringstream
rest;
225 else if(
split[0] ==
"stub")
227 std::ostringstream
rest;
232 else if(
split[0] ==
"remove")
234 if(
split.size() == 1)
237 if(
split[1] ==
"static")
241 "unexpected remove entry " +
split[1]);
245 "unexpected function entry " +
split[0]);
263 if(!
object.is_object())
271 if(!items.is_array())
288 if(
split[0] ==
"remove")
290 if(
split.size() == 1)
293 if(
split[1] ==
"static")
297 "unexpected remove entry " +
split[1]);
301 "unexpected object entry " +
split[0]);
327 argv.push_back(
"-I");
334 std::ostringstream result;
350 argv.push_back(
"-I");
354 std::ostringstream result;
361 defines.
parse(result.str());
382 if(t.text ==
"static")
385 out << std::string(6,
' ');
404 << defines(entry.content) <<
')';
406 std::map<std::string, std::string> loop_invariants;
409 loop_invariants[entry.loop_type + entry.identifier] = entry.content;
411 if(loop_invariants.empty())
423 const auto &token = *(t++);
429 const auto &invariant =
430 loop_invariants[
"while" + std::to_string(
while_count)];
432 if(!invariant.empty())
435 for(; t !=
t_end; t++)
438 << defines(invariant) <<
')';
441 else if(token ==
"for")
444 const auto &invariant =
445 loop_invariants[
"for" + std::to_string(
for_count)];
447 if(!invariant.empty())
450 for(; t !=
t_end; t++)
452 out <<
' ' <<
CPROVER_PREFIX <<
"invariant(" << defines(invariant)
471 if(t.text ==
"static")
474 out << std::string(6,
' ');
504 for(
const auto &entry :
config.functions)
506 if(std::regex_match(
name_opt->text, entry.first))
517 for(
const auto &entry :
config.objects)
519 if(std::regex_match(
name_opt->text, entry.first))
534 const std::string &in,
538 std::ostringstream out;
539 std::istringstream
in_str(in);
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.
assertiont(std::string _identifier, std::string _content)
contract_clauset(std::string _clause, std::string _content)
std::vector< loop_invariantt > loop_invariants
std::vector< assertiont > assertions
std::vector< contract_clauset > contract
optionalt< std::string > stub
loop_invariantt(std::string _loop_type, std::string _identifier, 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 &)