Skip to content

Partial revert of #1898 (always_inline support, second attempt) #2553

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Jul 8, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/ansi-c/always_inline1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
KNOWNBUG
main.c

^EXIT=0$
Expand Down
16 changes: 16 additions & 0 deletions regression/ansi-c/always_inline2/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
static inline __attribute__((__always_inline__)) int func(int val)
{
return val;
}

static inline int func2(int *p)
{
// the typecast, although redundant, is essential to show the problem
return func(*(int*)p);
}

int main()
{
int x;
return func2(&x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
12 changes: 12 additions & 0 deletions regression/ansi-c/always_inline3/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
static inline __attribute__((__always_inline__)) int func(int val)
{
if(val > 0)
return func(val - 1);
return 0;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline3/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
14 changes: 14 additions & 0 deletions regression/ansi-c/always_inline4/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
extern int func_alias(int val) __asm__("" "func");

static inline __attribute__((__always_inline__)) int func(int val)
{
if(val > 0)
return func_alias(val - 1);
return 0;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline4/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
12 changes: 12 additions & 0 deletions regression/ansi-c/always_inline5/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
static inline
__attribute__((__section__(".init"))) __attribute__((__always_inline__))
int func(int val)
{
return val + 1;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline5/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
10 changes: 10 additions & 0 deletions regression/ansi-c/always_inline6/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
static inline __attribute__((__always_inline__)) int func(int val, ...)
{
return val + 1;
}

int main()
{
int x;
return func(x, x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline6/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
11 changes: 11 additions & 0 deletions regression/ansi-c/always_inline7/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
static inline __attribute__((__always_inline__)) int func(int val)
{
int local = val;
return local;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline7/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
10 changes: 10 additions & 0 deletions regression/ansi-c/always_inline8/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
static inline __attribute__((__always_inline__)) int func(int val)
{
return (__typeof__(val))42;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline8/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
11 changes: 11 additions & 0 deletions regression/ansi-c/always_inline9/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
static inline __attribute__((__always_inline__)) int func(int val)
{
val = val + 1;
return val;
}

int main()
{
int x;
return func(x);
}
8 changes: 8 additions & 0 deletions regression/ansi-c/always_inline9/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE gcc-only
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$
24 changes: 24 additions & 0 deletions regression/cbmc/always_inline1/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#include <assert.h>

#ifndef __GNUC__
#define __attribute__(x)
#endif

static inline __attribute__((__always_inline__)) void func(int *val)
{
*val = 1;
return;
}

static inline int func2(int *p)
{
func(p);
return *p;
}

int main()
{
int x;
assert(func2(&x) == 1);
return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/always_inline1/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
30 changes: 30 additions & 0 deletions regression/cbmc/always_inline2/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
#include <assert.h>

#ifndef __GNUC__
#define __attribute__(x)
#endif

static inline __attribute__((__always_inline__)) int func(int *val)
{
switch(*val)
{
case 1:
return *val + 1;
case 2:
return *val + 2;
}

return *val;
}

static inline int func2(int *p)
{
return func(p);
}

int main()
{
int x = 1;
assert(func2(&x) == 2);
return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/always_inline2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
32 changes: 32 additions & 0 deletions regression/cbmc/always_inline3/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#include <assert.h>

#ifndef __GNUC__
#define __attribute__(x)
#endif

static inline __attribute__((__always_inline__)) void func(int *val)
{
if(*val < 0)
{
*val = 1;
return;
}
else
{
*val = 1;
return;
}
}

static inline int func2(int *p)
{
func(p);
return *p;
}

int main()
{
int x;
assert(func2(&x) == 1);
return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/always_inline3/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
2 changes: 0 additions & 2 deletions src/ansi-c/ansi_c_convert_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -171,8 +171,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
c_storage_spec.is_weak=true;
else if(type.id() == ID_used)
c_storage_spec.is_used = true;
else if(type.id() == ID_always_inline)
c_storage_spec.is_always_inline = true;
else if(type.id()==ID_auto)
{
// ignore
Expand Down
5 changes: 0 additions & 5 deletions src/ansi-c/ansi_c_declaration.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -81,8 +81,6 @@ void ansi_c_declarationt::output(std::ostream &out) const
out << " is_extern";
if(get_is_static_assert())
out << " is_static_assert";
if(get_is_always_inline())
out << " is_always_inline";
out << "\n";

out << "Type: " << type().pretty() << "\n";
Expand Down Expand Up @@ -166,9 +164,6 @@ void ansi_c_declarationt::to_symbol(
symbol.is_extern=false;
else if(get_is_extern()) // traditional GCC
symbol.is_file_local=true;

if(get_is_always_inline())
symbol.is_macro = true;
}

// GCC __attribute__((__used__)) - do not treat those as file-local
Expand Down
10 changes: 0 additions & 10 deletions src/ansi-c/ansi_c_declaration.h
Original file line number Diff line number Diff line change
Expand Up @@ -205,16 +205,6 @@ class ansi_c_declarationt:public exprt
set(ID_is_used, is_used);
}

bool get_is_always_inline() const
{
return get_bool(ID_is_always_inline);
}

void set_is_always_inline(bool is_always_inline)
{
set(ID_is_always_inline, is_always_inline);
}

void to_symbol(
const ansi_c_declaratort &,
symbolt &symbol) const;
Expand Down
2 changes: 0 additions & 2 deletions src/ansi-c/c_storage_spec.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,6 @@ void c_storage_spect::read(const typet &type)
is_weak=true;
else if(type.id() == ID_used)
is_used = true;
else if(type.id() == ID_always_inline)
is_always_inline = true;
else if(type.id()==ID_auto)
{
// ignore
Expand Down
9 changes: 2 additions & 7 deletions src/ansi-c/c_storage_spec.h
Original file line number Diff line number Diff line change
Expand Up @@ -36,14 +36,13 @@ class c_storage_spect
is_inline=false;
is_weak=false;
is_used = false;
is_always_inline = false;
alias.clear();
asm_label.clear();
section.clear();
}

bool is_typedef, is_extern, is_static, is_register, is_inline,
is_thread_local, is_weak, is_used, is_always_inline;
bool is_typedef, is_extern, is_static, is_register,
is_inline, is_thread_local, is_weak, is_used;

// __attribute__((alias("foo")))
irep_idt alias;
Expand All @@ -54,7 +53,6 @@ class c_storage_spect

bool operator==(const c_storage_spect &other) const
{
// clang-format off
return is_typedef==other.is_typedef &&
is_extern==other.is_extern &&
is_static==other.is_static &&
Expand All @@ -63,11 +61,9 @@ class c_storage_spect
is_inline==other.is_inline &&
is_weak==other.is_weak &&
is_used == other.is_used &&
is_always_inline == other.is_always_inline &&
alias==other.alias &&
asm_label==other.asm_label &&
section==other.section;
// clang-format on
}

bool operator!=(const c_storage_spect &other) const
Expand All @@ -85,7 +81,6 @@ class c_storage_spect
is_thread_local |=other.is_thread_local;
is_weak |=other.is_weak;
is_used |=other.is_used;
is_always_inline |= other.is_always_inline;
if(alias.empty())
alias=other.alias;
if(asm_label.empty())
Expand Down
Loading