Skip to content

Commit 48c5b10

Browse files
author
Daniel Kroening
committed
clean out langapi/languages.h
1 parent 9623503 commit 48c5b10

File tree

5 files changed

+26
-103
lines changed

5 files changed

+26
-103
lines changed

‎src/cbmc/bmc.cpp

+18-19
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,8 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/cprover_prefix.h>
2525

2626
#include <langapi/mode.h>
27-
#include <langapi/languages.h>
2827
#include <langapi/language_util.h>
2928

30-
#include <ansi-c/ansi_c_language.h>
31-
3229
#include <goto-programs/xml_goto_trace.h>
3330
#include <goto-programs/json_goto_trace.h>
3431
#include <goto-programs/graphml_witness.h>
@@ -222,8 +219,6 @@ void bmct::show_program()
222219
{
223220
unsigned count=1;
224221

225-
languagest languages(ns, new_ansi_c_language());
226-
227222
std::cout << "\n" << "Program constraints:" << "\n";
228223

229224
for(const auto &step : equation.SSA_steps)
@@ -233,13 +228,14 @@ void bmct::show_program()
233228

234229
if(step.is_assignment())
235230
{
236-
std::string string_value;
237-
languages.from_expr(step.cond_expr, string_value);
231+
std::string string_value=
232+
from_expr(ns, "", step.cond_expr);
238233
std::cout << "(" << count << ") " << string_value << "\n";
239234

240235
if(!step.guard.is_true())
241236
{
242-
languages.from_expr(step.guard, string_value);
237+
std::string string_value=
238+
from_expr(ns, "", step.guard);
243239
std::cout << std::string(std::to_string(count).size()+3, ' ');
244240
std::cout << "guard: " << string_value << "\n";
245241
}
@@ -248,14 +244,15 @@ void bmct::show_program()
248244
}
249245
else if(step.is_assert())
250246
{
251-
std::string string_value;
252-
languages.from_expr(step.cond_expr, string_value);
247+
std::string string_value=
248+
from_expr(ns, "", step.cond_expr);
253249
std::cout << "(" << count << ") ASSERT("
254250
<< string_value <<") " << "\n";
255251

256252
if(!step.guard.is_true())
257253
{
258-
languages.from_expr(step.guard, string_value);
254+
std::string string_value=
255+
from_expr(ns, "", step.guard);
259256
std::cout << std::string(std::to_string(count).size()+3, ' ');
260257
std::cout << "guard: " << string_value << "\n";
261258
}
@@ -264,14 +261,15 @@ void bmct::show_program()
264261
}
265262
else if(step.is_assume())
266263
{
267-
std::string string_value;
268-
languages.from_expr(step.cond_expr, string_value);
264+
std::string string_value=
265+
from_expr(ns, "", step.cond_expr);
269266
std::cout << "(" << count << ") ASSUME("
270267
<< string_value <<") " << "\n";
271268

272269
if(!step.guard.is_true())
273270
{
274-
languages.from_expr(step.guard, string_value);
271+
std::string string_value=
272+
from_expr(ns, "", step.guard);
275273
std::cout << std::string(std::to_string(count).size()+3, ' ');
276274
std::cout << "guard: " << string_value << "\n";
277275
}
@@ -280,24 +278,25 @@ void bmct::show_program()
280278
}
281279
else if(step.is_constraint())
282280
{
283-
std::string string_value;
284-
languages.from_expr(step.cond_expr, string_value);
281+
std::string string_value=
282+
from_expr(ns, "", step.cond_expr);
285283
std::cout << "(" << count << ") CONSTRAINT("
286284
<< string_value <<") " << "\n";
287285

288286
count++;
289287
}
290288
else if(step.is_shared_read() || step.is_shared_write())
291289
{
292-
std::string string_value;
293-
languages.from_expr(step.ssa_lhs, string_value);
290+
std::string string_value=
291+
from_expr(ns, "", step.ssa_lhs);
294292
std::cout << "(" << count << ") SHARED_"
295293
<< (step.is_shared_write()?"WRITE":"READ")
296294
<< "(" << string_value <<")\n";
297295

298296
if(!step.guard.is_true())
299297
{
300-
languages.from_expr(step.guard, string_value);
298+
std::string string_value=
299+
from_expr(ns, "", step.guard);
301300
std::cout << std::string(std::to_string(count).size()+3, ' ');
302301
std::cout << "guard: " << string_value << "\n";
303302
}

‎src/cbmc/show_vcc.cpp

+8-15
Original file line numberDiff line numberDiff line change
@@ -15,20 +15,15 @@ Author: Daniel Kroening, [email protected]
1515
#include <fstream>
1616

1717
#include <langapi/mode.h>
18-
#include <langapi/languages.h>
1918
#include <langapi/language_util.h>
2019

21-
#include <ansi-c/ansi_c_language.h>
22-
2320
#include <util/json.h>
2421
#include <util/json_expr.h>
2522

2623
void bmct::show_vcc_plain(std::ostream &out)
2724
{
2825
out << "\n" << "VERIFICATION CONDITIONS:" << "\n" << "\n";
2926

30-
languagest languages(ns, new_ansi_c_language());
31-
3227
bool has_threads=equation.has_threads();
3328

3429
for(symex_target_equationt::SSA_stepst::iterator
@@ -57,8 +52,8 @@ void bmct::show_vcc_plain(std::ostream &out)
5752
{
5853
if(!p_it->ignore)
5954
{
60-
std::string string_value;
61-
languages.from_expr(p_it->cond_expr, string_value);
55+
std::string string_value=
56+
from_expr(ns, "", p_it->cond_expr);
6257
out << "{-" << count << "} " << string_value << "\n";
6358

6459
#if 0
@@ -73,8 +68,8 @@ void bmct::show_vcc_plain(std::ostream &out)
7368

7469
out << "|--------------------------" << "\n";
7570

76-
std::string string_value;
77-
languages.from_expr(s_it->cond_expr, string_value);
71+
std::string string_value=
72+
from_expr(ns, "", s_it->cond_expr);
7873
out << "{" << 1 << "} " << string_value << "\n";
7974

8075
out << "\n";
@@ -87,8 +82,6 @@ void bmct::show_vcc_json(std::ostream &out)
8782

8883
json_arrayt &json_vccs=json_result["vccs"].make_array();
8984

90-
languagest languages(ns, new_ansi_c_language());
91-
9285
bool has_threads=equation.has_threads();
9386

9487
for(symex_target_equationt::SSA_stepst::iterator
@@ -125,14 +118,14 @@ void bmct::show_vcc_json(std::ostream &out)
125118
p_it->is_constraint()) &&
126119
!p_it->ignore)
127120
{
128-
std::string string_value;
129-
languages.from_expr(p_it->cond_expr, string_value);
121+
std::string string_value=
122+
from_expr(ns, "", p_it->cond_expr);
130123
json_constraints.push_back(json_stringt(string_value));
131124
}
132125
}
133126

134-
std::string string_value;
135-
languages.from_expr(s_it->cond_expr, string_value);
127+
std::string string_value=
128+
from_expr(ns, "", s_it->cond_expr);
136129
object["expression"]=json_stringt(string_value);
137130
}
138131

‎src/langapi/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
SRC = language_ui.cpp \
22
language_util.cpp \
3-
languages.cpp \
43
mode.cpp \
54
# Empty last line
65
INCLUDES= -I ..

‎src/langapi/languages.cpp

-20
This file was deleted.

‎src/langapi/languages.h

-48
This file was deleted.

0 commit comments

Comments
 (0)