Lines Matching defs:rodata
179 from target_objects import structs, rodata, sections, trace, printout
944 ro_name = self.smt_name ('rodata', kind = 'Fun')
945 imp_ro_name = self.smt_name ('implies-rodata', kind = 'Fun')
946 assert ro_name == 'rodata', repr (ro_name)
947 assert imp_ro_name == 'implies-rodata', repr (imp_ro_name)
948 [rodata_data, rodata_ranges, rodata_ptrs] = rodata
954 ro_witness = self.add_var ('rodata-witness', word32T)
955 ro_witness_val = self.add_var ('rodata-witness-val', word32T)
956 assert ro_witness == 'rodata-witness'
957 assert ro_witness_val == 'rodata-witness-val'
968 '(= (bvand rodata-witness #x00000003) #x00000000)']
972 self.send ('(define-fun rodata ((m %s)) Bool %s)' % (
974 self.send ('(define-fun implies-rodata ((m %s)) Bool %s)' % (
979 ro_witness = mk_smt_expr ('rodata-witness', word32T)
1683 [_, _, rodata_ptrs] = rodata