remove_library_assertions.cpp File Reference

#include <goto-programs/remove_library_assertions.h>
#include <langapi/mode.h>
#include <util/config/config.h>
#include <util/message/message.h>

Include dependency graph for remove_library_assertions.cpp:

Functions
void	remove_library_assertions (goto_functionst &goto_functions)
	Drop every assertion stated by ESBMC's own operational models, i.e.

Function Documentation

remove_library_assertions()

void remove_library_assertions

(

goto_functionst &

goto_functions

)

Drop every assertion stated by ESBMC's own operational models, i.e.

by a function whose body carries the __ESBMC_HIDE label. Must run before inlining: goto_inlinet rewrites the locations of a hidden function's instructions to the call site, after which model assertions are indistinguishable from the user's own. For the same reason a goto binary written with –full-inlining no longer has anything for this to remove.