[fpc-devel] Possibility to add a branch for experiment with formal annotation
We (Software Engineering Technology group of CS dept. at Technische
Universiteit Eindhoven) are working on an extension to (Free)Pascal,
by adding a facility for including formal annotation in programs
(pre/post conditions, invariants, etc).
We would also like to construct some tools for static analysis of (large)
Pascal programs. We investigated some options (continue with our own
tools, use an external framework, e.g. using a scanner/parser generator
like GOLD). Our conclusion is that FPC seems to be the most viable basis
in the longer run.
We would like to do our own development, i.e. make a branch of 2.0.4,
but retain the possibility to incorporate changes from the main FPC
development effort, and also have the possibility to give back our
work and have it incorporated into FPC (under the same license).
Currently, we have a separate source repository starting from 2.0.4,
and we have extended FreePascal minimally with syntax like
{@ boolean-expression}
to mean something like 'while not boolean-expression do' (i.e. the
program hangs if the condition does not hold). This experiment
was carried out to determine how easy it is to adapt the scanner,
parser, and code generator.
QUESTION: Would it be possible for us to obtain a branch in the FPC
subverion repository for our work? That would simplify both the
incorporation (merging) of changes from the FPC team, and vice versa.
Or do you have alternative suggestions?
Can we contact someone off-list to discuss this further?
Best regards,
Tom Verhoeff
--
E-MAIL: T.Verhoeff @ TUE.NL | Fac. of Math. Computing Science
PHONE: +31 40 247 41 25| Eindhoven University of Technology
FAX:+31 40 247 54 04| PO Box 513, NL-5600 MB Eindhoven
http://www.win.tue.nl/~wstomv/ | The Netherlands
___
fpc-devel maillist - fpc-devel@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-devel
Re: [fpc-devel] Possibility to add a branch for experiment with formal annotation
Tom Verhoeff wrote:
We (Software Engineering Technology group of CS dept. at Technische
Universiteit Eindhoven) are working on an extension to (Free)Pascal,
by adding a facility for including formal annotation in programs
(pre/post conditions, invariants, etc).
We would also like to construct some tools for static analysis of (large)
Pascal programs. We investigated some options (continue with our own
tools, use an external framework, e.g. using a scanner/parser generator
like GOLD). Our conclusion is that FPC seems to be the most viable basis
in the longer run.
We would like to do our own development, i.e. make a branch of 2.0.4,
but retain the possibility to incorporate changes from the main FPC
development effort, and also have the possibility to give back our
work and have it incorporated into FPC (under the same license).
Currently, we have a separate source repository starting from 2.0.4,
and we have extended FreePascal minimally with syntax like
{@ boolean-expression}
to mean something like 'while not boolean-expression do' (i.e. the
program hangs if the condition does not hold). This experiment
was carried out to determine how easy it is to adapt the scanner,
parser, and code generator.
QUESTION: Would it be possible for us to obtain a branch in the FPC
subverion repository for our work?
Yes.
That would simplify both the
incorporation (merging) of changes from the FPC team, and vice versa.
Or do you have alternative suggestions?
Can we contact someone off-list to discuss this further?
Contact me.
Best regards,
Tom Verhoeff
___
fpc-devel maillist - fpc-devel@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-devel
[fpc-devel] Suggestion for change: Overly strict check
Hi all. I was hoping there could be a discussion of a certain feature in FPC, which doesn't work very well for us. Ultimately, I would like to see it gone completely. It's a very small extra-strong syntax check, appearantly implemented to avoid bad code. However, it's not entirely obvious why this is supposed to help. Please consider this example: type tfoo = class(tbar) private public procedure Frob(); procedure Wait(delay: integer); procedure ReadStuff(buffer: tbuffer; wait: boolean); end; When declaring classes or interfaces, it is specifically checked that the names of methods are NOT the same as _any_ variable name of _any_ other method in the class. This means that the example above will NOT compile. Now, in Delphi mode this check is not performed, and so the code above will compile without problems. The reason for keeping this check, as far as I know, is that it's supposed to lead to better code. For instance, in the body of ReadStuff(), the identifier wait could be potentially confused between the boolean parameter, and the procedure(delay: integer) of object;. At least, that's the theory. Of cours, if the parameter wait was a function (delay: integer) of object, there could be some confusion. This is very rare, however - and you have to be careful anyway, because this restriction is not consistent: var wait: boolean; procedure tfoo.ReadStuff(buffer: tbuffer; wait: boolean); begin // In here, wait could refer either to the parameter, or the global var. end; However, it's not confused with the global var, because standard scoping rules apply. Same as with inner functions and such. Also, if you have a unit foo, with a variable bar, you can use foo.bar to refer to that specific var. However, foo.bar could also refer to the local record foo with the field bar. Again, standard scoping rules solve this problem without incident. The _real_ problem, however, is that with these very strict checks we essentially only have one namespace for each class/interface. All function names, parameter names AND local variable names share ONE namespace, with the one exception that no check is performed between functions. We have several examples where good, standard names are used for functions, and then cannot be used in local variables - this is even though they could never be confused in any realistic scenario. We urge you to rethink the introduction of these checks. It's making it tremendeously difficult for us to change our code to objfpc mode, and removing it would not break a single line of code anywhere. We have to rethink quite many variable and/or function names, because many good names are already taken. This is, in effect, making our code quality slightly worse overall. What are your thoughts on this? -- Regards, Christian Iversen, Ivo Steinmann ___ fpc-devel maillist - fpc-devel@lists.freepascal.org http://lists.freepascal.org/mailman/listinfo/fpc-devel
Re: [fpc-devel] Suggestion for change: Overly strict check
Am Mittwoch, 27. September 2006 22:36 schrieb Christian Iversen: Hi all. I was hoping there could be a discussion of a certain feature in FPC, which doesn't work very well for us. Ultimately, I would like to see it gone completely. It's a very small extra-strong syntax check, appearantly implemented to avoid bad code. However, it's not entirely obvious why this is supposed to help. Please consider this example: type tfoo = class(tbar) private public procedure Frob(); procedure Wait(delay: integer); procedure ReadStuff(buffer: tbuffer; wait: boolean); end; Even in delphi, I allways use(d) procedure ReadStuff(aBuffer: tbuffer; aWait: boolean); .. This won't help you, but you asked for thought. And my thoughts are: I like it the way it is. regards Burkhard ___ fpc-devel maillist - fpc-devel@lists.freepascal.org http://lists.freepascal.org/mailman/listinfo/fpc-devel
Re: [fpc-devel] Suggestion for change: Overly strict check
Hi,
Let me give you an example of a real bug that allow attackers to gain
root access using X-server, and I hope you will understand why such
checking can be a good thing.
On C you can have a function and a variable with the same name, and
the only way that you can make a difference, is to use the () signs.
So anything without () is variable.
Now, on X-server there was the following (bad coding style as well) of
(I'm using my memory here)
...
if (owner == getchown) { ...
..
Now the bug was that they did not place () in getchown, so it looked
for a data that on this case was 0 like the owenr that had 0 for
root. so if someone arrived to that code position, they would have
been able to use the content (that execute things if I remember it
right) to execute their own code under root privliges.
I think that what you have talked about allow you to easily avoid such
problems. Beside, a non formal way to write parameters is to add a
so await is good in one location and wait in another location.
I do agree, that this type of check can be come smarter, but I do see
a need for it.
Another good thing in Pascal, is that you have namespaces for
everything (almost), so unlike C, you can actually can guess what
variable/paramter you are using, if you do it smart enough. ('with
a,b,c do' is not a good way imho).
Ido
On 9/27/06, Christian Iversen [EMAIL PROTECTED] wrote:
Hi all.
I was hoping there could be a discussion of a certain feature in FPC, which
doesn't work very well for us. Ultimately, I would like to see it gone
completely. It's a very small extra-strong syntax check, appearantly
implemented to avoid bad code. However, it's not entirely obvious why this is
supposed to help.
Please consider this example:
type
tfoo = class(tbar)
private
public
procedure Frob();
procedure Wait(delay: integer);
procedure ReadStuff(buffer: tbuffer; wait: boolean);
end;
When declaring classes or interfaces, it is specifically checked that the
names of methods are NOT the same as _any_ variable name of _any_ other
method in the class. This means that the example above will NOT compile.
Now, in Delphi mode this check is not performed, and so the code above will
compile without problems.
The reason for keeping this check, as far as I know, is that it's supposed to
lead to better code. For instance, in the body of ReadStuff(), the
identifier wait could be potentially confused between the boolean
parameter, and the procedure(delay: integer) of object;.
At least, that's the theory. Of cours, if the parameter wait was a function
(delay: integer) of object, there could be some confusion. This is very
rare, however - and you have to be careful anyway, because this restriction
is not consistent:
var
wait: boolean;
procedure tfoo.ReadStuff(buffer: tbuffer; wait: boolean);
begin
// In here, wait could refer either to the parameter, or the global var.
end;
However, it's not confused with the global var, because standard scoping rules
apply. Same as with inner functions and such. Also, if you have a unit foo,
with a variable bar, you can use foo.bar to refer to that specific var.
However, foo.bar could also refer to the local record foo with the
field bar. Again, standard scoping rules solve this problem without
incident.
The _real_ problem, however, is that with these very strict checks we
essentially only have one namespace for each class/interface. All function
names, parameter names AND local variable names share ONE namespace, with the
one exception that no check is performed between functions.
We have several examples where good, standard names are used for functions,
and then cannot be used in local variables - this is even though they could
never be confused in any realistic scenario.
We urge you to rethink the introduction of these checks. It's making it
tremendeously difficult for us to change our code to objfpc mode, and
removing it would not break a single line of code anywhere. We have to
rethink quite many variable and/or function names, because many good names
are already taken. This is, in effect, making our code quality slightly worse
overall.
What are your thoughts on this?
--
Regards,
Christian Iversen,
Ivo Steinmann
___
fpc-devel maillist - fpc-devel@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-devel
___
fpc-devel maillist - fpc-devel@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-devel
