Skip to content

Commit af24891

Browse files
author
Wei Ming Khoo
committed
#46: Remove duplicate declarations
1 parent 176a532 commit af24891

File tree

4 files changed

+14
-6
lines changed

4 files changed

+14
-6
lines changed

tnt_include.h

+5-5
Original file line numberDiff line numberDiff line change
@@ -255,15 +255,15 @@ extern void TNT_(check_var_access)(ThreadId tid, const HChar* varname, Int var_r
255255
#define VARNAMESIZE 1024
256256
// These arrays are initialised to 0 in TNT_(clo_post_init)
257257
// Tmp variable indices; the MSB indicates whether it's tainted (1) or not (0)
258-
UInt *ti;
258+
extern UInt *ti;
259259
// Tmp variable values
260-
ULong *tv;
260+
extern ULong *tv;
261261
// Reg variable indices; values are obtained in real-time
262-
UInt *ri;
262+
extern UInt *ri;
263263
// Tmp variable Types/Widths
264-
UInt *tt;
264+
extern UInt *tt;
265265
// Stores the variable name derived from describe_data()
266-
HChar *varname;
266+
extern HChar *varname;
267267

268268
#define _ti(ltmp) ti[ltmp] & 0x7fffffff
269269
#define is_tainted(ltmp) (ti[ltmp] >> 31)

tnt_main.c

+6
Original file line numberDiff line numberDiff line change
@@ -3906,6 +3906,12 @@ static int tnt_isatty(void)
39063906
return 0;
39073907
}
39083908

3909+
UInt *ti;
3910+
ULong *tv;
3911+
UInt *ri;
3912+
UInt *tt;
3913+
HChar *varname;
3914+
39093915
static void tnt_post_clo_init(void)
39103916
{
39113917
if(*TNT_(clo_file_filter) == '\0'){

tnt_smt2.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ const Int SMT2_ty[] = {
3232
};
3333

3434
// Array for tracking tmp variable types
35-
UInt *tt; //[TI_MAX];
35+
extern UInt *tt; //[TI_MAX];
3636

3737
void TNT_(smt2_preamble)()
3838
{

tnt_syswrap.c

+2
Original file line numberDiff line numberDiff line change
@@ -237,6 +237,8 @@ void read_common ( UInt taint_offset, Int taint_len,
237237
TNT_(make_mem_tainted)( addr, len );
238238
}
239239

240+
extern HChar *varname;
241+
240242
void TNT_(syscall_read)(ThreadId tid, UWord* args, UInt nArgs,
241243
SysRes res) {
242244
// ssize_t read(int fildes, void *buf, size_t nbyte);

0 commit comments

Comments
 (0)