git.iko.soy/Idris-dev
on master help sign in
Added test for incorrect FFI C usage.
b9a7352Jan de Muijnck-Hughes
test/TestData.hs+10−8
compare with master
unifiedsplit
@@ -114,14 +114,16 @@ testFamiliesData = [
114 ( 8, ANY ),
114 ( 8, ANY ),
115 ( 9, ANY )]),
115 ( 9, ANY )]),
116 ("ffi", "FFI",
116 ("ffi", "FFI",
117− [ ( 1, ANY ),
117+ [ ( 1, ANY )
118− ( 2, ANY ),
118+ , ( 2, ANY )
119− ( 3, ANY ),
119+ , ( 3, ANY )
120− ( 4, ANY ),
120+ , ( 4, ANY )
121− ( 5, ANY ),
121+ , ( 5, ANY )
122− ( 6, C_CG ),
122+ , ( 6, C_CG )
123− ( 7, C_CG ),
123+ , ( 7, C_CG )
124− ( 8, C_CG )]),
124+ , ( 8, C_CG )
125+ , ( 9, C_CG )
126+ ]),
125 ("folding", "Folding",
127 ("folding", "Folding",
126 [ ( 1, ANY )]),
128 [ ( 1, ANY )]),
127 ("idrisdoc", "Idris documentation",
129 ("idrisdoc", "Idris documentation",
test/ffi009/Bad.idrnew file+36
@@ -0,0 +1,36 @@
1+module Bad
2+
3+%include c "ffi009.h"
4+
5+private
6+get_allocation_size : Ptr -> IO Int
7+get_allocation_size = foreign FFI_C "get_allocation_size" (Ptr -> IO Int)
8+
9+-- [ NOTE ]
10+--
11+-- As `commen_call` is a partial function and not inline, Idris should complain.
12+
13+private
14+common_call : String -> Int -> IO ManagedPtr
15+common_call f l = do
16+ ptr <- foreign FFI_C
17+ f
18+ (Int -> IO Ptr)
19+ l
20+ len <- get_allocation_size ptr
21+ pure (prim__registerPtr ptr len)
22+
23+func_foo : IO ManagedPtr
24+func_foo = common_call "foo" 4
25+
26+func_bar : IO ManagedPtr
27+func_bar = common_call "bar" 8
28+
29+
30+namespace Main
31+ main : IO ()
32+ main = do
33+ foo <- func_foo
34+ bar <- func_bar
35+
36+ printLn "I should not be seen."
test/ffi009/Good.idrnew file+37
@@ -0,0 +1,37 @@
1+module Good
2+
3+%include c "ffi009.h"
4+
5+private
6+get_allocation_size : Ptr -> IO Int
7+get_allocation_size = foreign FFI_C "get_allocation_size" (Ptr -> IO Int)
8+
9+-- [ NOTE ]
10+--
11+-- As `commen_call` is a partial function and not inline, Idris should complain.
12+
13+private
14+%inline
15+common_call : String -> Int -> IO ManagedPtr
16+common_call f l = do
17+ ptr <- foreign FFI_C
18+ f
19+ (Int -> IO Ptr)
20+ l
21+ len <- get_allocation_size ptr
22+ pure (prim__registerPtr ptr len)
23+
24+func_foo : IO ManagedPtr
25+func_foo = common_call "foo" 4
26+
27+func_bar : IO ManagedPtr
28+func_bar = common_call "bar" 8
29+
30+
31+namespace Main
32+ main : IO ()
33+ main = do
34+ foo <- func_foo
35+ bar <- func_bar
36+
37+ printLn "I should be seen."
test/ffi009/expectednew file+1
@@ -0,0 +1 @@
1+"I should be seen."
test/ffi009/ffi009.cnew file+44
@@ -0,0 +1,44 @@
1+#include "ffi009.h"
2+
3+
4+Vect* foo(int length)
5+{
6+ return new_empty_vect(length);
7+}
8+
9+Vect* bar(int length)
10+{
11+ return new_empty_vect(length * 2);
12+}
13+
14+
15+Vect* new_empty_vect(int l)
16+{
17+ unsigned char* vect;
18+
19+ vect = malloc(sizeof(unsigned char) * l);
20+
21+ if (vect == NULL){
22+ free(vect);
23+ return NULL;
24+ }
25+
26+ Vect* v = malloc(sizeof(Vect));
27+
28+ if (v==NULL){
29+ free(vect);
30+ free(v);
31+ return NULL;
32+ }
33+
34+ v->value = vect;
35+ v->length = l;
36+
37+ return v;
38+}
39+
40+
41+int get_allocation_size(Vect* v)
42+{
43+ return sizeof(Vect) + v->length;
44+}
test/ffi009/ffi009.hnew file+20
@@ -0,0 +1,20 @@
1+#ifndef FFI009_H
2+#define FFI009_H
3+
4+#include <idris_rts.h>
5+
6+
7+typedef struct
8+{
9+ unsigned char* value;
10+ int length;
11+} Vect;
12+
13+int get_allocation_size(Vect* v);
14+
15+Vect* new_empty_vect(int length);
16+
17+Vect* foo(int length);
18+Vect* bar(int length);
19+
20+#endif /* FFI009_H */
test/ffi009/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ Bad.idr -o bad --cg-opt "ffi009.c" --cg-opt "-fno-strict-overflow"
3+${IDRIS:-idris} $@ Good.idr -o good --cg-opt "ffi009.c"
4+./good
5+rm -f *.ibc good