Packages/c/cbmc-doc-6.9.0-1.fc45.x86_64.rpm

/*******************************************************************\


Module: Validate code


Author: Daniel Poetzl


\*******************************************************************/


#ifndef CPROVER_UTIL_VALIDATE_CODE_H

#define CPROVER_UTIL_VALIDATE_CODE_H


class codet;

class namespacet;

enum class validation_modet;


void check_code(const codet &code, const validation_modet vm);


void validate_code(

  const codet &code,

  const namespacet &ns,

  const validation_modet vm);


void validate_full_code(

  const codet &code,

  const namespacet &ns,

  const validation_modet vm);


#endif /* CPROVER_UTIL_VALIDATE_CODE_H */

codet
Data structure for representing an arbitrary statement in a program.
Definition std_code_base.h:29

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

validate_code
void validate_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed, assuming that all its enclosed statements,...
Definition validate_code.cpp:84

validate_full_code
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
Definition validate_code.cpp:100

check_code
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...
Definition validate_code.cpp:70

validation_modet
validation_modet
Definition validation_mode.h:13