User Tools

Site Tools


retrieve_information_from_source_code

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

retrieve_information_from_source_code [2013/07/15 11:11] (current)
lliang created
Line 1: Line 1:
 +Suppose you have the following string array in the source code:
  
 +<​code>​char* string_array[] = ["​hello",​ "​world"​];</​code>​
 +
 +We can retrieve the string values from the array as follows:
 +
 +<​code>​
 +// lookup the symbol table
 +// note: the id parameter of the lookup function should start with the prefix c:: 
 +// in this case it will be c:: followed by the variable name string_array
 +const symbolt &​string_array_symbol=ns.lookup("​c::​string_array"​);​
 +
 +// translate the symbol to the proper type
 +array_exprt string_array_expr=to_array_expr(string_array_symbol.value);​
 +
 +// iterate through the string values ​
 +forall_operands(string_value_it,​ string_array_expr)
 +{
 +  // include the header file <​ansi-c/​string_constant.h>​ in order to use the to_string_constant function
 +  irep_idt string_value=to_string_constant(string_value_it->​op0().op0()).get_value();​
 +  std::cout << string_value << std::endl;
 +}
 +</​code>​
 +
 +Similarly, if you have an integer array in the source code such as 
 +
 +<​code>​int int_array = [1, 2, 3];</​code>​
 +
 +We can get the values of it in CBMC as follows:
 +
 +<​code>​
 +const symbolt &​int_array_symbol=ns.lookup("​c::​int_array"​);​
 +
 +// translate the symbol to the proper type
 +array_exprt int_array_expr=to_array_expr(int_array_symbol.value);​
 +
 +// iterate through the string values ​
 +forall_operands(int_value_it,​ int_array_expr)
 +{
 +  // include the header file <​util/​arith_tools.h>​ in order to use the to_integer function
 +  mp_integer int_value;
 +  to_integer(*int_value_it,​ int_value);
 +}
 +</​code>​
retrieve_information_from_source_code.txt ยท Last modified: 2013/07/15 11:11 by lliang